InvalidNamePartBar.agda:1,19-19
InvalidNamePartBar.agda:1,19: in the name _|_, the part | is not valid because it is used for with-arguments
→<ERROR>
 Set
...
